T:Type, l1, l2:T List, x:T. l1  l2 @ [x]  l1  l2  l1 = (l2 @ [x]) 

latex

Definitions	P & Q, x:A. B(x), t  T, x:A. B(x), l1  l2, {T}, P  Q, as @ bs, Prop, ||as||, P  Q, P  Q, P  Q, True, T, False, b
Lemmas	iseg weakening, cons iseg, iseg nil, squash wf, true wf, iff functionality wrt iff, iseg append iff, length wf1, append wf, iseg wf